Variables/arrays

A global variable is defined using the following syntax,

var knight = 0;

wherevar is a key word for defining a variable and knight is the variable name. Initially, knight has the value 0. Semi-colon is used to mark the end of the 'sentence' as above. We remark the input language of PAT is weakly typed and therefore no typing information is required when declaring a variable. Cast between incompatible types may result in a run-time exception.

A fixed-size array may be defined as follows,

var board = [3, 5, 6, 0, 2, 7, 8, 4, 1];

where board is the array name and its initial value is specified as the sequence, e.g., board[0] = 3. The following defines an array of size 3.

var leader[3];

All elements in the array are initialized to be 0.

Note: Currently, channel array is not supported in this module.

Note for multi-dimensional array: PAT supports multi-dimensional arrays by converting them into one dimensional arrays. You can declare and use multi-dimensional arrays as follows (Note that here, the N should be a constant). The only restriction is that you can not assign multi-dimensional array constant to multi-dimensional arrays variables. To initialize a multi-dimensional array, you need to do it explicitly in some events.

• var matrix[3*N][10];

Note: To assign values to specific elements in an array, you can use event prefix. For example:

 P() = a { matrix[1][9] = 0 } -> Skip;

Variable range specification: users can provide the range of the variables/arrays explicitly by giving lower bound or upper bound or both. In this way, the model checkers and simulator can report the out-of-range violation of the variable values to help users to monitor the variable values. The syntax of specifying range values are demonstrated as follows.

• var knight : {0..} = 0;
• var board : {0..10} = [3, 5, 6, 0, 2, 7, 8, 4, 1];
• var leader[N] : {..N-1}; //where N is a constant defined.

Array Initialization: To ease the modeling, PAT supports fast array initialization using following syntax.

• #define N 2;
• var array = [1(2), 3..6, 7(N*2), 12..10];
• //the above is same as the following
• var array = [1, 1, 3, 4, 5, 6, 7, 7, 7, 7, 12, 11, 10];

In the above syntax, 1(2) and 7(N*2) allow user to quickly create an array with same initial values. 3..6 and 12..10 allow user to write quick increasing and decreasing loop to initialize the array.

Random Initialization: You may want to let the program to choose a random value for a variable or elements in an array. In this case, you may want to try WildConstant Symbol *.

• var knight : {0..10} = *;
• var board : {0..10} = *;

in the above syntax, the variable knight and all elements in the array board will be initialized with a random value in the range of 0 to 10.

Note: This feature can only be used for symbolic model checking using BDD. Simulating models with WildConstant symbol will cause exception. In the verification window, explicit model checking algorithms will not be available for models with WildConstant symbol. 

Channels

wherechannel is a key word for declaring channels only, c is the channel name and 5 is the channel buffer size; Channel buffer size must be greater or equal to 0. Notice that a channel with buffer size 0 sends/receives messages synchronously. This is used to model pair-wise synchronization, which involves two parties. Barrier-synchronization, which involves multiple parties, is supported by following CSP's approach, i.e., alphabetized parallel composition.  

Propositions

In addition, the key word #define may be used to define propositions. For instance,

#define goal x == 0;

where goal is the name of the proposition and x == 0 is what goal means. A proposition name is used in the same way as global constant is used. For instance, given the above definition, we may write the following,

if (goal) { P } else { Q };

which means if the value of x is 0 then do P else do Q. We remark that propositions are the basic elements of LTL formulae.